class Test {
     int y <= 4;
     int setYValue(int newY) {
          pre: y>0;
          post: y<10;
          y <= newY;
          return 0;
     }
     static void main() {
		// show abstract syntax tree
		int x <= (2-3)*4;

		// long  
		long l;
		l <= 2L + 2;

		// function call
		x <= new Child().f1(3);

		// array
		int[] intArray <= new int[10];
		intArray[0] <= 5;
		
		long[] longArray <= [intArray[0], l, x];

		// length
		int len <= intArray.length;
    }		
}

// inherit
class Child extends Parent{
	// field
	int f;
	
	int f1(int a) {
        pre:a>0;
        post: a>0;

		// parent field
       	a <= p; 

		boolean b;
		b <= false;
		
		// while expression
		while (a>0){
			// override field
			int f <= 8;
		}
		
		// this function call
		a <= this.f2(b);

      	return a;
	}

	// another function
	 int f2(boolean b){
		pre:b;

		// post cond
		post: b;

		return 0;
	}
}

class Parent{
	int p;
}